for clients C sends FIFO
forfrom j to i via (S[j,i],codes)
forreceives at i via (R[i],decodes)  requests Req[j] are acknowledged by Ack[j,i]
== i:C.
== f:{e:E| R(i,e)} {e:E| j:C. (S(j,i,e))} 
== (e.j:C. (S(j,i,e))  f e.R(i,e)
== & (e:{e:E| R(i,e)} , j:{j:C| S(j,i,f(e))} .
== & (decodes(i,e,(state when e)) = codes(j,i,f(e),(state when f(e))))
== & (e, e':{e:E| R(i,e)} , j:C. (S(j,i,f(e)))  (S(j,i,f(e')))  f(e) c f(e')  e c e')
== & (j:C.
== & (req:{e:E| Ack(j,i,e)} {e:E| S(j,i,e) & Req(j,e)} 
== & ((e.S(j,i,e) & Req(j,e)  req e.Ack(j,i,e)
== & (& (a:{e:E| Ack(j,i,e)} . e:{e:E| R(i,e)} . (f(e) = req(a) & e c a))
== & (& e.req(e) is c< preserving on e.Ack(j,i,e)))) 

latex

---

clarification:

fifo+(es;codes;decodes;C;S;R;T;Req;Ack)
== i:C.
== f:{e:es-E(es)| R(i,e)} {e:es-E(es)| j:C. (S(j,i,e))} 
== (antecedent-surjection(es;e.R(i,e);e.j:C. (S(j,i,e));f)
== & (e:{e:es-E(es)| R(i,e)} , j:{j:C| S(j,i,f(e))} .
== & (decodes(i,e,es-state-when(es;e)) = codes(j,i,f(e),es-state-when(es;f(e)))  T)
== & (e:{e:es-E(es)| R(i,e)} , e':{e:es-E(es)| R(i,e)} , j:C.
== & ((S(j,i,f(e)))  (S(j,i,f(e')))  es-causle(es;f(e);f(e'))  es-causle(es;e;e'))
== & (j:C.
== & (req:{e:es-E(es)| Ack(j,i,e)} {e:es-E(es)| S(j,i,e) & Req(j,e)} 
== & ((antecedent-surjection(es;e.Ack(j,i,e);e.S(j,i,e) & Req(j,e);req)
== & (& (a:{e:es-E(es)| Ack(j,i,e)} .
== & (& (e:{e:es-E(es)| R(i,e)} . (f(e) = req(a)  es-E(es) & es-causle(es;e;a)))
== & (& causal-order-preserving(es;e.req(e);e.Ack(j,i,e))))) 

latex

Definitions	(state when e), P  Q, x:AB(x), Q  f P, x.A(x), x:A. B(x), x:A. B(x), {x:A| B(x)} , P & Q, s = t, E, e c e', a.f(a) is c< preserving on e.P(e), f(a)
FDL editor aliases	fifo+